$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$Prop). ($\exists$$l$:$T$ List. $P$($l$)) $\Rightarrow$ safety($T$;$x$.$P$($x$)) $\Rightarrow$ $P$(nil)